<!DOCTYPE html>
<html class="writer-html5" lang="en" data-content_root="./">
<head>
  <meta charset="utf-8" /><meta name="viewport" content="width=device-width, initial-scale=1" />

  <meta name="viewport" content="width=device-width, initial-scale=1.0" />
  <title>12. Differential Calculus &mdash; Mathematics in Lean v4.19.0 documentation</title>
      <link rel="stylesheet" type="text/css" href="_static/pygments.css?v=80d5e7a1" />
      <link rel="stylesheet" type="text/css" href="_static/css/theme.css?v=19f00094" />
      <link rel="stylesheet" type="text/css" href="_static/css/custom.css?v=0731ccc3" />

  
    <link rel="shortcut icon" href="_static/favicon.ico"/>
  <!--[if lt IE 9]>
    <script src="_static/js/html5shiv.min.js"></script>
  <![endif]-->
  
        <script src="_static/jquery.js?v=5d32c60e"></script>
        <script src="_static/_sphinx_javascript_frameworks_compat.js?v=2cd50e6c"></script>
        <script src="_static/documentation_options.js?v=7048e04d"></script>
        <script src="_static/doctools.js?v=9a2dae69"></script>
        <script src="_static/sphinx_highlight.js?v=dc90522c"></script>
        <script async="async" src="https://cdn.jsdelivr.net/npm/mathjax@3/es5/tex-mml-chtml.js"></script>
    <script src="_static/js/theme.js"></script>
    <link rel="index" title="Index" href="genindex.html" />
    <link rel="search" title="Search" href="search.html" />
    <link rel="next" title="13. Integration and Measure Theory" href="C13_Integration_and_Measure_Theory.html" />
    <link rel="prev" title="11. Topology" href="C11_Topology.html" /> 
</head>

<body class="wy-body-for-nav"> 
  <div class="wy-grid-for-nav">
    <nav data-toggle="wy-nav-shift" class="wy-nav-side">
      <div class="wy-side-scroll">
        <div class="wy-side-nav-search" >

          
          
          <a href="index.html" class="icon icon-home">
            Mathematics in Lean
          </a>
<div role="search">
  <form id="rtd-search-form" class="wy-form" action="search.html" method="get">
    <input type="text" name="q" placeholder="Search docs" aria-label="Search docs" />
    <input type="hidden" name="check_keywords" value="yes" />
    <input type="hidden" name="area" value="default" />
  </form>
</div>
        </div><div class="wy-menu wy-menu-vertical" data-spy="affix" role="navigation" aria-label="Navigation menu">
              <ul class="current">
<li class="toctree-l1"><a class="reference internal" href="C01_Introduction.html">1. Introduction</a></li>
<li class="toctree-l1"><a class="reference internal" href="C02_Basics.html">2. Basics</a></li>
<li class="toctree-l1"><a class="reference internal" href="C03_Logic.html">3. Logic</a></li>
<li class="toctree-l1"><a class="reference internal" href="C04_Sets_and_Functions.html">4. Sets and Functions</a></li>
<li class="toctree-l1"><a class="reference internal" href="C05_Elementary_Number_Theory.html">5. Elementary Number Theory</a></li>
<li class="toctree-l1"><a class="reference internal" href="C06_Discrete_Mathematics.html">6. Discrete Mathematics</a></li>
<li class="toctree-l1"><a class="reference internal" href="C07_Structures.html">7. Structures</a></li>
<li class="toctree-l1"><a class="reference internal" href="C08_Hierarchies.html">8. Hierarchies</a></li>
<li class="toctree-l1"><a class="reference internal" href="C09_Groups_and_Rings.html">9. Groups and Rings</a></li>
<li class="toctree-l1"><a class="reference internal" href="C10_Linear_Algebra.html">10. Linear algebra</a></li>
<li class="toctree-l1"><a class="reference internal" href="C11_Topology.html">11. Topology</a></li>
<li class="toctree-l1 current"><a class="current reference internal" href="#">12. Differential Calculus</a><ul>
<li class="toctree-l2"><a class="reference internal" href="#elementary-differential-calculus">12.1. Elementary Differential Calculus</a></li>
<li class="toctree-l2"><a class="reference internal" href="#differential-calculus-in-normed-spaces">12.2. Differential Calculus in Normed Spaces</a><ul>
<li class="toctree-l3"><a class="reference internal" href="#id3">12.2.1. Normed spaces</a></li>
<li class="toctree-l3"><a class="reference internal" href="#continuous-linear-maps">12.2.2. Continuous linear maps</a></li>
<li class="toctree-l3"><a class="reference internal" href="#asymptotic-comparisons">12.2.3. Asymptotic comparisons</a></li>
<li class="toctree-l3"><a class="reference internal" href="#differentiability">12.2.4. Differentiability</a></li>
</ul>
</li>
</ul>
</li>
<li class="toctree-l1"><a class="reference internal" href="C13_Integration_and_Measure_Theory.html">13. Integration and Measure Theory</a></li>
</ul>
<ul>
<li class="toctree-l1"><a class="reference internal" href="genindex.html">Index</a></li>
</ul>

        </div>
      </div>
    </nav>

    <section data-toggle="wy-nav-shift" class="wy-nav-content-wrap"><nav class="wy-nav-top" aria-label="Mobile navigation menu" >
          <i data-toggle="wy-nav-top" class="fa fa-bars"></i>
          <a href="index.html">Mathematics in Lean</a>
      </nav>

      <div class="wy-nav-content">
        <div class="rst-content">
          <div role="navigation" aria-label="Page navigation">
  <ul class="wy-breadcrumbs">
      <li><a href="index.html" class="icon icon-home" aria-label="Home"></a></li>
      <li class="breadcrumb-item active"><span class="section-number">12. </span>Differential Calculus</li>
      <li class="wy-breadcrumbs-aside">
            <a href="_sources/C12_Differential_Calculus.rst.txt" rel="nofollow"> View page source</a>
      </li>
  </ul>
  <hr/>
</div>
          <div role="main" class="document" itemscope="itemscope" itemtype="http://schema.org/Article">
           <div itemprop="articleBody">
             
  <section id="index-0">
<span id="differential-calculus"></span><span id="id1"></span><h1><span class="section-number">12. </span>Differential Calculus<a class="headerlink" href="#index-0" title="Link to this heading">&#61633;</a></h1>
<p>We now consider the formalization of notions from <em>analysis</em>,
starting with differentiation in this chapter
and turning integration and measure theory in the next.
In <a class="reference internal" href="#elementary-differential-calculus"><span class="std std-numref">Section 12.1</span></a>, we stick with the
setting of functions from the real numbers to the real numbers,
which is familiar from any introductory calculus class.
In <a class="reference internal" href="#normed-spaces"><span class="std std-numref">Section 12.2</span></a>, we then consider the notion of a derivative in
a much broader setting.</p>
<section id="elementary-differential-calculus">
<span id="index-1"></span><span id="id2"></span><h2><span class="section-number">12.1. </span>Elementary Differential Calculus<a class="headerlink" href="#elementary-differential-calculus" title="Link to this heading">&#61633;</a></h2>
<p>Let <code class="docutils literal notranslate"><span class="pre">f</span></code> be a function from the reals to the reals. There is a difference
between talking about the derivative of <code class="docutils literal notranslate"><span class="pre">f</span></code> at a single point and
talking about the derivative function.
In Mathlib, the first notion is represented as follows.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kn">open</span><span class="w"> </span><span class="n">Real</span>

<span class="sd">/-- The sin function has derivative 1 at 0. -/</span>
<span class="kd">example</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">HasDerivAt</span><span class="w"> </span><span class="n">sin</span><span class="w"> </span><span class="mi">1</span><span class="w"> </span><span class="mi">0</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span><span class="w"> </span><span class="n">simpa</span><span class="w"> </span><span class="n">using</span><span class="w"> </span><span class="n">hasDerivAt_sin</span><span class="w"> </span><span class="mi">0</span>
</pre></div>
</div>
<p>We can also express that <code class="docutils literal notranslate"><span class="pre">f</span></code> is differentiable at a point without
specifying its derivative there
by writing <code class="docutils literal notranslate"><span class="pre">DifferentiableAt</span> <span class="pre">&#8477;</span></code>.
We specify <code class="docutils literal notranslate"><span class="pre">&#8477;</span></code> explicitly because in a slightly more general context,
when talking about functions from <code class="docutils literal notranslate"><span class="pre">&#8450;</span></code> to <code class="docutils literal notranslate"><span class="pre">&#8450;</span></code>,
we want to be able to distinguish between being differentiable in the real sense
and being differentiable in the sense of the complex derivative.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span><span class="w"> </span><span class="o">(</span><span class="n">x</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#8477;</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">DifferentiableAt</span><span class="w"> </span><span class="n">&#8477;</span><span class="w"> </span><span class="n">sin</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="o">(</span><span class="n">hasDerivAt_sin</span><span class="w"> </span><span class="n">x</span><span class="o">)</span><span class="bp">.</span><span class="n">differentiableAt</span>
</pre></div>
</div>
<p>It would be inconvenient to have to provide a proof of differentiability
every time we want to refer to a derivative.
So Mathlib provides a function <code class="docutils literal notranslate"><span class="pre">deriv</span> <span class="pre">f</span> <span class="pre">:</span> <span class="pre">&#8477;</span> <span class="pre">&#8594;</span> <span class="pre">&#8477;</span></code> that is defined for any
function <code class="docutils literal notranslate"><span class="pre">f</span> <span class="pre">:</span> <span class="pre">&#8477;</span> <span class="pre">&#8594;</span> <span class="pre">&#8477;</span></code>
but is defined to take the value <code class="docutils literal notranslate"><span class="pre">0</span></code> at any point where <code class="docutils literal notranslate"><span class="pre">f</span></code> is not differentiable.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span><span class="w"> </span><span class="o">{</span><span class="n">f</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#8477;</span><span class="w"> </span><span class="bp">&#8594;</span><span class="w"> </span><span class="n">&#8477;</span><span class="o">}</span><span class="w"> </span><span class="o">{</span><span class="n">x</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#8477;</span><span class="o">}</span><span class="w"> </span><span class="o">(</span><span class="n">h</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">HasDerivAt</span><span class="w"> </span><span class="n">f</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="n">x</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">deriv</span><span class="w"> </span><span class="n">f</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="n">h.deriv</span>

<span class="kd">example</span><span class="w"> </span><span class="o">{</span><span class="n">f</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#8477;</span><span class="w"> </span><span class="bp">&#8594;</span><span class="w"> </span><span class="n">&#8477;</span><span class="o">}</span><span class="w"> </span><span class="o">{</span><span class="n">x</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#8477;</span><span class="o">}</span><span class="w"> </span><span class="o">(</span><span class="n">h</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="bp">&#172;</span><span class="n">DifferentiableAt</span><span class="w"> </span><span class="n">&#8477;</span><span class="w"> </span><span class="n">f</span><span class="w"> </span><span class="n">x</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">deriv</span><span class="w"> </span><span class="n">f</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="mi">0</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="n">deriv_zero_of_not_differentiableAt</span><span class="w"> </span><span class="n">h</span>
</pre></div>
</div>
<p>Of course there are many lemmas about <code class="docutils literal notranslate"><span class="pre">deriv</span></code> that do require differentiability assumptions.
For instance, you should think about a counterexample to the next lemma without the
differentiability assumptions.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span><span class="w"> </span><span class="o">{</span><span class="n">f</span><span class="w"> </span><span class="n">g</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#8477;</span><span class="w"> </span><span class="bp">&#8594;</span><span class="w"> </span><span class="n">&#8477;</span><span class="o">}</span><span class="w"> </span><span class="o">{</span><span class="n">x</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#8477;</span><span class="o">}</span><span class="w"> </span><span class="o">(</span><span class="n">hf</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">DifferentiableAt</span><span class="w"> </span><span class="n">&#8477;</span><span class="w"> </span><span class="n">f</span><span class="w"> </span><span class="n">x</span><span class="o">)</span><span class="w"> </span><span class="o">(</span><span class="n">hg</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">DifferentiableAt</span><span class="w"> </span><span class="n">&#8477;</span><span class="w"> </span><span class="n">g</span><span class="w"> </span><span class="n">x</span><span class="o">)</span><span class="w"> </span><span class="o">:</span>
<span class="w">    </span><span class="n">deriv</span><span class="w"> </span><span class="o">(</span><span class="n">f</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="n">g</span><span class="o">)</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">deriv</span><span class="w"> </span><span class="n">f</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="n">deriv</span><span class="w"> </span><span class="n">g</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="n">deriv_add</span><span class="w"> </span><span class="n">hf</span><span class="w"> </span><span class="n">hg</span>
</pre></div>
</div>
<p>Interestingly, however, there are statements that can avoid differentiability
assumptions by taking advantage
of the fact that the value of <code class="docutils literal notranslate"><span class="pre">deriv</span></code> defaults to zero when the function is
not differentiable.
So making sense of the following statement requires knowing the precise
definition of <code class="docutils literal notranslate"><span class="pre">deriv</span></code>.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span><span class="w"> </span><span class="o">{</span><span class="n">f</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#8477;</span><span class="w"> </span><span class="bp">&#8594;</span><span class="w"> </span><span class="n">&#8477;</span><span class="o">}</span><span class="w"> </span><span class="o">{</span><span class="n">a</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#8477;</span><span class="o">}</span><span class="w"> </span><span class="o">(</span><span class="n">h</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">IsLocalMin</span><span class="w"> </span><span class="n">f</span><span class="w"> </span><span class="n">a</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">deriv</span><span class="w"> </span><span class="n">f</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="mi">0</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="n">h.deriv_eq_zero</span>
</pre></div>
</div>
<p>We can even state Rolle&#8217;s theorem without any differentiability assumptions, which
seems even weirder.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kn">open</span><span class="w"> </span><span class="n">Set</span>

<span class="kd">example</span><span class="w"> </span><span class="o">{</span><span class="n">f</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#8477;</span><span class="w"> </span><span class="bp">&#8594;</span><span class="w"> </span><span class="n">&#8477;</span><span class="o">}</span><span class="w"> </span><span class="o">{</span><span class="n">a</span><span class="w"> </span><span class="n">b</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#8477;</span><span class="o">}</span><span class="w"> </span><span class="o">(</span><span class="n">hab</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="bp">&lt;</span><span class="w"> </span><span class="n">b</span><span class="o">)</span><span class="w"> </span><span class="o">(</span><span class="n">hfc</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">ContinuousOn</span><span class="w"> </span><span class="n">f</span><span class="w"> </span><span class="o">(</span><span class="n">Icc</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="n">b</span><span class="o">))</span><span class="w"> </span><span class="o">(</span><span class="n">hfI</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">f</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">f</span><span class="w"> </span><span class="n">b</span><span class="o">)</span><span class="w"> </span><span class="o">:</span>
<span class="w">    </span><span class="bp">&#8707;</span><span class="w"> </span><span class="n">c</span><span class="w"> </span><span class="bp">&#8712;</span><span class="w"> </span><span class="n">Ioo</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="n">b</span><span class="o">,</span><span class="w"> </span><span class="n">deriv</span><span class="w"> </span><span class="n">f</span><span class="w"> </span><span class="n">c</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="mi">0</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="n">exists_deriv_eq_zero</span><span class="w"> </span><span class="n">hab</span><span class="w"> </span><span class="n">hfc</span><span class="w"> </span><span class="n">hfI</span>
</pre></div>
</div>
<p>Of course, this trick does not work for the general mean value theorem.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span><span class="w"> </span><span class="o">(</span><span class="n">f</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#8477;</span><span class="w"> </span><span class="bp">&#8594;</span><span class="w"> </span><span class="n">&#8477;</span><span class="o">)</span><span class="w"> </span><span class="o">{</span><span class="n">a</span><span class="w"> </span><span class="n">b</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#8477;</span><span class="o">}</span><span class="w"> </span><span class="o">(</span><span class="n">hab</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="bp">&lt;</span><span class="w"> </span><span class="n">b</span><span class="o">)</span><span class="w"> </span><span class="o">(</span><span class="n">hf</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">ContinuousOn</span><span class="w"> </span><span class="n">f</span><span class="w"> </span><span class="o">(</span><span class="n">Icc</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="n">b</span><span class="o">))</span>
<span class="w">    </span><span class="o">(</span><span class="n">hf&#39;</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">DifferentiableOn</span><span class="w"> </span><span class="n">&#8477;</span><span class="w"> </span><span class="n">f</span><span class="w"> </span><span class="o">(</span><span class="n">Ioo</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="n">b</span><span class="o">))</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="bp">&#8707;</span><span class="w"> </span><span class="n">c</span><span class="w"> </span><span class="bp">&#8712;</span><span class="w"> </span><span class="n">Ioo</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="n">b</span><span class="o">,</span><span class="w"> </span><span class="n">deriv</span><span class="w"> </span><span class="n">f</span><span class="w"> </span><span class="n">c</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="o">(</span><span class="n">f</span><span class="w"> </span><span class="n">b</span><span class="w"> </span><span class="bp">-</span><span class="w"> </span><span class="n">f</span><span class="w"> </span><span class="n">a</span><span class="o">)</span><span class="w"> </span><span class="bp">/</span><span class="w"> </span><span class="o">(</span><span class="n">b</span><span class="w"> </span><span class="bp">-</span><span class="w"> </span><span class="n">a</span><span class="o">)</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="n">exists_deriv_eq_slope</span><span class="w"> </span><span class="n">f</span><span class="w"> </span><span class="n">hab</span><span class="w"> </span><span class="n">hf</span><span class="w"> </span><span class="n">hf&#39;</span>
</pre></div>
</div>
<p>Lean can automatically compute some simple derivatives using the <code class="docutils literal notranslate"><span class="pre">simp</span></code> tactic.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">deriv</span><span class="w"> </span><span class="o">(</span><span class="k">fun</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#8477;</span><span class="w"> </span><span class="bp">&#8614;</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="bp">^</span><span class="w"> </span><span class="mi">5</span><span class="o">)</span><span class="w"> </span><span class="mi">6</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="mi">5</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="mi">6</span><span class="w"> </span><span class="bp">^</span><span class="w"> </span><span class="mi">4</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span><span class="w"> </span><span class="n">simp</span>

<span class="kd">example</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">deriv</span><span class="w"> </span><span class="n">sin</span><span class="w"> </span><span class="n">&#960;</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="bp">-</span><span class="mi">1</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span><span class="w"> </span><span class="n">simp</span>
</pre></div>
</div>
</section>
<section id="differential-calculus-in-normed-spaces">
<span id="normed-spaces"></span><span id="index-2"></span><h2><span class="section-number">12.2. </span>Differential Calculus in Normed Spaces<a class="headerlink" href="#differential-calculus-in-normed-spaces" title="Link to this heading">&#61633;</a></h2>
<section id="id3">
<h3><span class="section-number">12.2.1. </span>Normed spaces<a class="headerlink" href="#id3" title="Link to this heading">&#61633;</a></h3>
<p>Differentiation can be generalized beyond <code class="docutils literal notranslate"><span class="pre">&#8477;</span></code> using the notion of a
<em>normed vector space</em>, which encapsulates both direction and distance.
We start with the notion of a <em>normed group</em>, which is an additive commutative
group equipped with a real-valued norm function
satisfying the following conditions.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">variable</span><span class="w"> </span><span class="o">{</span><span class="n">E</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="kt">Type</span><span class="bp">*</span><span class="o">}</span><span class="w"> </span><span class="o">[</span><span class="n">NormedAddCommGroup</span><span class="w"> </span><span class="n">E</span><span class="o">]</span>

<span class="kd">example</span><span class="w"> </span><span class="o">(</span><span class="n">x</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">E</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="mi">0</span><span class="w"> </span><span class="bp">&#8804;</span><span class="w"> </span><span class="bp">&#8214;</span><span class="n">x</span><span class="bp">&#8214;</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="n">norm_nonneg</span><span class="w"> </span><span class="n">x</span>

<span class="kd">example</span><span class="w"> </span><span class="o">{</span><span class="n">x</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">E</span><span class="o">}</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="bp">&#8214;</span><span class="n">x</span><span class="bp">&#8214;</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="mi">0</span><span class="w"> </span><span class="bp">&#8596;</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="mi">0</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="n">norm_eq_zero</span>

<span class="kd">example</span><span class="w"> </span><span class="o">(</span><span class="n">x</span><span class="w"> </span><span class="n">y</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">E</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="bp">&#8214;</span><span class="n">x</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="n">y</span><span class="bp">&#8214;</span><span class="w"> </span><span class="bp">&#8804;</span><span class="w"> </span><span class="bp">&#8214;</span><span class="n">x</span><span class="bp">&#8214;</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="bp">&#8214;</span><span class="n">y</span><span class="bp">&#8214;</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="n">norm_add_le</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="n">y</span>
</pre></div>
</div>
<p>Every normed space is a metric space with distance function
<span class="math notranslate nohighlight">\(d(x, y) = \| x - y \|\)</span>, and hence it is also a topological space.
Lean and Mathlib know this.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">MetricSpace</span><span class="w"> </span><span class="n">E</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span><span class="w"> </span><span class="n">infer_instance</span>

<span class="kd">example</span><span class="w"> </span><span class="o">{</span><span class="n">X</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="kt">Type</span><span class="bp">*</span><span class="o">}</span><span class="w"> </span><span class="o">[</span><span class="n">TopologicalSpace</span><span class="w"> </span><span class="n">X</span><span class="o">]</span><span class="w"> </span><span class="o">{</span><span class="n">f</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">X</span><span class="w"> </span><span class="bp">&#8594;</span><span class="w"> </span><span class="n">E</span><span class="o">}</span><span class="w"> </span><span class="o">(</span><span class="n">hf</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Continuous</span><span class="w"> </span><span class="n">f</span><span class="o">)</span><span class="w"> </span><span class="o">:</span>
<span class="w">    </span><span class="n">Continuous</span><span class="w"> </span><span class="k">fun</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="bp">&#8614;</span><span class="w"> </span><span class="bp">&#8214;</span><span class="n">f</span><span class="w"> </span><span class="n">x</span><span class="bp">&#8214;</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="n">hf.norm</span>
</pre></div>
</div>
<p>In order to use the notion of a norm with concepts from linear algebra,
we add the assumption <code class="docutils literal notranslate"><span class="pre">NormedSpace</span> <span class="pre">&#8477;</span> <span class="pre">E</span></code> on top of <code class="docutils literal notranslate"><span class="pre">NormedAddGroup</span> <span class="pre">E</span></code>.
This stipulates that <code class="docutils literal notranslate"><span class="pre">E</span></code> is a vector space over <code class="docutils literal notranslate"><span class="pre">&#8477;</span></code> and that
scalar multiplication satisfies the following condition.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">variable</span><span class="w"> </span><span class="o">[</span><span class="n">NormedSpace</span><span class="w"> </span><span class="n">&#8477;</span><span class="w"> </span><span class="n">E</span><span class="o">]</span>

<span class="kd">example</span><span class="w"> </span><span class="o">(</span><span class="n">a</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#8477;</span><span class="o">)</span><span class="w"> </span><span class="o">(</span><span class="n">x</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">E</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="bp">&#8214;</span><span class="n">a</span><span class="w"> </span><span class="bp">&#8226;</span><span class="w"> </span><span class="n">x</span><span class="bp">&#8214;</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="bp">|</span><span class="n">a</span><span class="bp">|</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="bp">&#8214;</span><span class="n">x</span><span class="bp">&#8214;</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="n">norm_smul</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="n">x</span>
</pre></div>
</div>
<p>A complete normed space is known as a <em>Banach space</em>.
Every finite-dimensional vector space is complete.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span><span class="w"> </span><span class="o">[</span><span class="n">FiniteDimensional</span><span class="w"> </span><span class="n">&#8477;</span><span class="w"> </span><span class="n">E</span><span class="o">]</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">CompleteSpace</span><span class="w"> </span><span class="n">E</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span><span class="w"> </span><span class="n">infer_instance</span>
</pre></div>
</div>
<p>In all the previous examples, we used the real numbers as the base field.
More generally, we can make sense of calculus with a vector space over any
<em>nontrivially normed field</em>. These are fields that are equipped with a
real-valued norm that is multiplicative and has the property that
not every element has norm zero or one
(equivalently, there is an element whose norm is bigger than one).</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span><span class="w"> </span><span class="o">(</span><span class="n">&#120156;</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="kt">Type</span><span class="bp">*</span><span class="o">)</span><span class="w"> </span><span class="o">[</span><span class="n">NontriviallyNormedField</span><span class="w"> </span><span class="n">&#120156;</span><span class="o">]</span><span class="w"> </span><span class="o">(</span><span class="n">x</span><span class="w"> </span><span class="n">y</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#120156;</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="bp">&#8214;</span><span class="n">x</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="n">y</span><span class="bp">&#8214;</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="bp">&#8214;</span><span class="n">x</span><span class="bp">&#8214;</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="bp">&#8214;</span><span class="n">y</span><span class="bp">&#8214;</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="n">norm_mul</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="n">y</span>

<span class="kd">example</span><span class="w"> </span><span class="o">(</span><span class="n">&#120156;</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="kt">Type</span><span class="bp">*</span><span class="o">)</span><span class="w"> </span><span class="o">[</span><span class="n">NontriviallyNormedField</span><span class="w"> </span><span class="n">&#120156;</span><span class="o">]</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="bp">&#8707;</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#120156;</span><span class="o">,</span><span class="w"> </span><span class="mi">1</span><span class="w"> </span><span class="bp">&lt;</span><span class="w"> </span><span class="bp">&#8214;</span><span class="n">x</span><span class="bp">&#8214;</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="n">NormedField.exists_one_lt_norm</span><span class="w"> </span><span class="n">&#120156;</span>
</pre></div>
</div>
<p>A finite-dimensional vector space over a nontrivially normed field is
complete as long as the field itself is complete.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span><span class="w"> </span><span class="o">(</span><span class="n">&#120156;</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="kt">Type</span><span class="bp">*</span><span class="o">)</span><span class="w"> </span><span class="o">[</span><span class="n">NontriviallyNormedField</span><span class="w"> </span><span class="n">&#120156;</span><span class="o">]</span><span class="w"> </span><span class="o">(</span><span class="n">E</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="kt">Type</span><span class="bp">*</span><span class="o">)</span><span class="w"> </span><span class="o">[</span><span class="n">NormedAddCommGroup</span><span class="w"> </span><span class="n">E</span><span class="o">]</span>
<span class="w">    </span><span class="o">[</span><span class="n">NormedSpace</span><span class="w"> </span><span class="n">&#120156;</span><span class="w"> </span><span class="n">E</span><span class="o">]</span><span class="w"> </span><span class="o">[</span><span class="n">CompleteSpace</span><span class="w"> </span><span class="n">&#120156;</span><span class="o">]</span><span class="w"> </span><span class="o">[</span><span class="n">FiniteDimensional</span><span class="w"> </span><span class="n">&#120156;</span><span class="w"> </span><span class="n">E</span><span class="o">]</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">CompleteSpace</span><span class="w"> </span><span class="n">E</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="n">FiniteDimensional.complete</span><span class="w"> </span><span class="n">&#120156;</span><span class="w"> </span><span class="n">E</span>
</pre></div>
</div>
</section>
<section id="continuous-linear-maps">
<h3><span class="section-number">12.2.2. </span>Continuous linear maps<a class="headerlink" href="#continuous-linear-maps" title="Link to this heading">&#61633;</a></h3>
<p>We now turn to the morphisms in the category of normed spaces, namely,
continuous linear maps.
In Mathlib, the type of <code class="docutils literal notranslate"><span class="pre">&#120156;</span></code>-linear continuous maps between normed spaces
<code class="docutils literal notranslate"><span class="pre">E</span></code> and <code class="docutils literal notranslate"><span class="pre">F</span></code> is written <code class="docutils literal notranslate"><span class="pre">E</span> <span class="pre">&#8594;L[&#120156;]</span> <span class="pre">F</span></code>.
They are implemented as <em>bundled maps</em>, which means that an element of this type
a structure that that includes the function itself and the properties
of being linear and continuous.
Lean will insert a coercion so that a continuous linear map can be treated
as a function.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">variable</span><span class="w"> </span><span class="o">{</span><span class="n">&#120156;</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="kt">Type</span><span class="bp">*</span><span class="o">}</span><span class="w"> </span><span class="o">[</span><span class="n">NontriviallyNormedField</span><span class="w"> </span><span class="n">&#120156;</span><span class="o">]</span><span class="w"> </span><span class="o">{</span><span class="n">E</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="kt">Type</span><span class="bp">*</span><span class="o">}</span><span class="w"> </span><span class="o">[</span><span class="n">NormedAddCommGroup</span><span class="w"> </span><span class="n">E</span><span class="o">]</span>
<span class="w">  </span><span class="o">[</span><span class="n">NormedSpace</span><span class="w"> </span><span class="n">&#120156;</span><span class="w"> </span><span class="n">E</span><span class="o">]</span><span class="w"> </span><span class="o">{</span><span class="n">F</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="kt">Type</span><span class="bp">*</span><span class="o">}</span><span class="w"> </span><span class="o">[</span><span class="n">NormedAddCommGroup</span><span class="w"> </span><span class="n">F</span><span class="o">]</span><span class="w"> </span><span class="o">[</span><span class="n">NormedSpace</span><span class="w"> </span><span class="n">&#120156;</span><span class="w"> </span><span class="n">F</span><span class="o">]</span>

<span class="kd">example</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">E</span><span class="w"> </span><span class="bp">&#8594;</span><span class="n">L</span><span class="o">[</span><span class="n">&#120156;</span><span class="o">]</span><span class="w"> </span><span class="n">E</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="n">ContinuousLinearMap.id</span><span class="w"> </span><span class="n">&#120156;</span><span class="w"> </span><span class="n">E</span>

<span class="kd">example</span><span class="w"> </span><span class="o">(</span><span class="n">f</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">E</span><span class="w"> </span><span class="bp">&#8594;</span><span class="n">L</span><span class="o">[</span><span class="n">&#120156;</span><span class="o">]</span><span class="w"> </span><span class="n">F</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">E</span><span class="w"> </span><span class="bp">&#8594;</span><span class="w"> </span><span class="n">F</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="n">f</span>

<span class="kd">example</span><span class="w"> </span><span class="o">(</span><span class="n">f</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">E</span><span class="w"> </span><span class="bp">&#8594;</span><span class="n">L</span><span class="o">[</span><span class="n">&#120156;</span><span class="o">]</span><span class="w"> </span><span class="n">F</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Continuous</span><span class="w"> </span><span class="n">f</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="n">f.cont</span>

<span class="kd">example</span><span class="w"> </span><span class="o">(</span><span class="n">f</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">E</span><span class="w"> </span><span class="bp">&#8594;</span><span class="n">L</span><span class="o">[</span><span class="n">&#120156;</span><span class="o">]</span><span class="w"> </span><span class="n">F</span><span class="o">)</span><span class="w"> </span><span class="o">(</span><span class="n">x</span><span class="w"> </span><span class="n">y</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">E</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">f</span><span class="w"> </span><span class="o">(</span><span class="n">x</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="n">y</span><span class="o">)</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">f</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="n">f</span><span class="w"> </span><span class="n">y</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="n">f.map_add</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="n">y</span>

<span class="kd">example</span><span class="w"> </span><span class="o">(</span><span class="n">f</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">E</span><span class="w"> </span><span class="bp">&#8594;</span><span class="n">L</span><span class="o">[</span><span class="n">&#120156;</span><span class="o">]</span><span class="w"> </span><span class="n">F</span><span class="o">)</span><span class="w"> </span><span class="o">(</span><span class="n">a</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#120156;</span><span class="o">)</span><span class="w"> </span><span class="o">(</span><span class="n">x</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">E</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">f</span><span class="w"> </span><span class="o">(</span><span class="n">a</span><span class="w"> </span><span class="bp">&#8226;</span><span class="w"> </span><span class="n">x</span><span class="o">)</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="bp">&#8226;</span><span class="w"> </span><span class="n">f</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="n">f.map_smul</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="n">x</span>
</pre></div>
</div>
<p>Continuous linear maps have an operator norm that is characterized by the
following properties.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">variable</span><span class="w"> </span><span class="o">(</span><span class="n">f</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">E</span><span class="w"> </span><span class="bp">&#8594;</span><span class="n">L</span><span class="o">[</span><span class="n">&#120156;</span><span class="o">]</span><span class="w"> </span><span class="n">F</span><span class="o">)</span>

<span class="kd">example</span><span class="w"> </span><span class="o">(</span><span class="n">x</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">E</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="bp">&#8214;</span><span class="n">f</span><span class="w"> </span><span class="n">x</span><span class="bp">&#8214;</span><span class="w"> </span><span class="bp">&#8804;</span><span class="w"> </span><span class="bp">&#8214;</span><span class="n">f</span><span class="bp">&#8214;</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="bp">&#8214;</span><span class="n">x</span><span class="bp">&#8214;</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="n">f.le_opNorm</span><span class="w"> </span><span class="n">x</span>

<span class="kd">example</span><span class="w"> </span><span class="o">{</span><span class="n">M</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#8477;</span><span class="o">}</span><span class="w"> </span><span class="o">(</span><span class="n">hMp</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="mi">0</span><span class="w"> </span><span class="bp">&#8804;</span><span class="w"> </span><span class="n">M</span><span class="o">)</span><span class="w"> </span><span class="o">(</span><span class="n">hM</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="bp">&#8704;</span><span class="w"> </span><span class="n">x</span><span class="o">,</span><span class="w"> </span><span class="bp">&#8214;</span><span class="n">f</span><span class="w"> </span><span class="n">x</span><span class="bp">&#8214;</span><span class="w"> </span><span class="bp">&#8804;</span><span class="w"> </span><span class="n">M</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="bp">&#8214;</span><span class="n">x</span><span class="bp">&#8214;</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="bp">&#8214;</span><span class="n">f</span><span class="bp">&#8214;</span><span class="w"> </span><span class="bp">&#8804;</span><span class="w"> </span><span class="n">M</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="n">f.opNorm_le_bound</span><span class="w"> </span><span class="n">hMp</span><span class="w"> </span><span class="n">hM</span>
</pre></div>
</div>
<p>There is also a notion of bundled continuous linear <em>isomorphism</em>.
Their type of such isomorphisms is <code class="docutils literal notranslate"><span class="pre">E</span> <span class="pre">&#8771;L[&#120156;]</span> <span class="pre">F</span></code>.</p>
<p>As a challenging exercise, you can prove the Banach-Steinhaus theorem, also
known as the Uniform Boundedness Principle.
The principle states that a family of continuous linear maps from a Banach space
into a normed space is pointwise
bounded, then the norms of these linear maps are uniformly bounded.
The main ingredient is Baire&#8217;s theorem
<code class="docutils literal notranslate"><span class="pre">nonempty_interior_of_iUnion_of_closed</span></code>. (You proved a version of this in the topology chapter.)
Minor ingredients include <code class="docutils literal notranslate"><span class="pre">continuous_linear_map.opNorm_le_of_shell</span></code>,
<code class="docutils literal notranslate"><span class="pre">interior_subset</span></code> and <code class="docutils literal notranslate"><span class="pre">interior_iInter_subset</span></code> and <code class="docutils literal notranslate"><span class="pre">isClosed_le</span></code>.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">variable</span><span class="w"> </span><span class="o">{</span><span class="n">&#120156;</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="kt">Type</span><span class="bp">*</span><span class="o">}</span><span class="w"> </span><span class="o">[</span><span class="n">NontriviallyNormedField</span><span class="w"> </span><span class="n">&#120156;</span><span class="o">]</span><span class="w"> </span><span class="o">{</span><span class="n">E</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="kt">Type</span><span class="bp">*</span><span class="o">}</span><span class="w"> </span><span class="o">[</span><span class="n">NormedAddCommGroup</span><span class="w"> </span><span class="n">E</span><span class="o">]</span>
<span class="w">  </span><span class="o">[</span><span class="n">NormedSpace</span><span class="w"> </span><span class="n">&#120156;</span><span class="w"> </span><span class="n">E</span><span class="o">]</span><span class="w"> </span><span class="o">{</span><span class="n">F</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="kt">Type</span><span class="bp">*</span><span class="o">}</span><span class="w"> </span><span class="o">[</span><span class="n">NormedAddCommGroup</span><span class="w"> </span><span class="n">F</span><span class="o">]</span><span class="w"> </span><span class="o">[</span><span class="n">NormedSpace</span><span class="w"> </span><span class="n">&#120156;</span><span class="w"> </span><span class="n">F</span><span class="o">]</span>

<span class="kn">open</span><span class="w"> </span><span class="n">Metric</span>

<span class="kd">example</span><span class="w"> </span><span class="o">{</span><span class="n">&#953;</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="kt">Type</span><span class="bp">*</span><span class="o">}</span><span class="w"> </span><span class="o">[</span><span class="n">CompleteSpace</span><span class="w"> </span><span class="n">E</span><span class="o">]</span><span class="w"> </span><span class="o">{</span><span class="n">g</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#953;</span><span class="w"> </span><span class="bp">&#8594;</span><span class="w"> </span><span class="n">E</span><span class="w"> </span><span class="bp">&#8594;</span><span class="n">L</span><span class="o">[</span><span class="n">&#120156;</span><span class="o">]</span><span class="w"> </span><span class="n">F</span><span class="o">}</span><span class="w"> </span><span class="o">(</span><span class="n">h</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="bp">&#8704;</span><span class="w"> </span><span class="n">x</span><span class="o">,</span><span class="w"> </span><span class="bp">&#8707;</span><span class="w"> </span><span class="n">C</span><span class="o">,</span><span class="w"> </span><span class="bp">&#8704;</span><span class="w"> </span><span class="n">i</span><span class="o">,</span><span class="w"> </span><span class="bp">&#8214;</span><span class="n">g</span><span class="w"> </span><span class="n">i</span><span class="w"> </span><span class="n">x</span><span class="bp">&#8214;</span><span class="w"> </span><span class="bp">&#8804;</span><span class="w"> </span><span class="n">C</span><span class="o">)</span><span class="w"> </span><span class="o">:</span>
<span class="w">    </span><span class="bp">&#8707;</span><span class="w"> </span><span class="n">C&#39;</span><span class="o">,</span><span class="w"> </span><span class="bp">&#8704;</span><span class="w"> </span><span class="n">i</span><span class="o">,</span><span class="w"> </span><span class="bp">&#8214;</span><span class="n">g</span><span class="w"> </span><span class="n">i</span><span class="bp">&#8214;</span><span class="w"> </span><span class="bp">&#8804;</span><span class="w"> </span><span class="n">C&#39;</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">  </span><span class="c1">-- sequence of subsets consisting of those `x : E` with norms `&#8214;g i x&#8214;` bounded by `n`</span>
<span class="w">  </span><span class="k">let</span><span class="w"> </span><span class="n">e</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#8469;</span><span class="w"> </span><span class="bp">&#8594;</span><span class="w"> </span><span class="n">Set</span><span class="w"> </span><span class="n">E</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="k">fun</span><span class="w"> </span><span class="n">n</span><span class="w"> </span><span class="bp">&#8614;</span><span class="w"> </span><span class="bp">&#8898;</span><span class="w"> </span><span class="n">i</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#953;</span><span class="o">,</span><span class="w"> </span><span class="o">{</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">E</span><span class="w"> </span><span class="bp">|</span><span class="w"> </span><span class="bp">&#8214;</span><span class="n">g</span><span class="w"> </span><span class="n">i</span><span class="w"> </span><span class="n">x</span><span class="bp">&#8214;</span><span class="w"> </span><span class="bp">&#8804;</span><span class="w"> </span><span class="n">n</span><span class="w"> </span><span class="o">}</span>
<span class="w">  </span><span class="c1">-- each of these sets is closed</span>
<span class="w">  </span><span class="k">have</span><span class="w"> </span><span class="n">hc</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="bp">&#8704;</span><span class="w"> </span><span class="n">n</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#8469;</span><span class="o">,</span><span class="w"> </span><span class="n">IsClosed</span><span class="w"> </span><span class="o">(</span><span class="n">e</span><span class="w"> </span><span class="n">n</span><span class="o">)</span>
<span class="w">  </span><span class="gr">sorry</span>
<span class="w">  </span><span class="c1">-- the union is the entire space; this is where we use `h`</span>
<span class="w">  </span><span class="k">have</span><span class="w"> </span><span class="n">hU</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="o">(</span><span class="bp">&#8899;</span><span class="w"> </span><span class="n">n</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#8469;</span><span class="o">,</span><span class="w"> </span><span class="n">e</span><span class="w"> </span><span class="n">n</span><span class="o">)</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">univ</span>
<span class="w">  </span><span class="gr">sorry</span>
<span class="w">  </span><span class="c">/-</span><span class="cm"> apply the Baire category theorem to conclude that for some `m : &#8469;`,</span>
<span class="cm">       `e m` contains some `x` -/</span>
<span class="w">  </span><span class="n">obtain</span><span class="w"> </span><span class="o">&#10216;</span><span class="n">m</span><span class="o">,</span><span class="w"> </span><span class="n">x</span><span class="o">,</span><span class="w"> </span><span class="n">hx</span><span class="o">&#10217;</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="bp">&#8707;</span><span class="w"> </span><span class="n">m</span><span class="o">,</span><span class="w"> </span><span class="bp">&#8707;</span><span class="w"> </span><span class="n">x</span><span class="o">,</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="bp">&#8712;</span><span class="w"> </span><span class="n">interior</span><span class="w"> </span><span class="o">(</span><span class="n">e</span><span class="w"> </span><span class="n">m</span><span class="o">)</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="gr">sorry</span>
<span class="w">  </span><span class="n">obtain</span><span class="w"> </span><span class="o">&#10216;</span><span class="n">&#949;</span><span class="o">,</span><span class="w"> </span><span class="n">&#949;_pos</span><span class="o">,</span><span class="w"> </span><span class="n">h&#949;</span><span class="o">&#10217;</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="bp">&#8707;</span><span class="w"> </span><span class="n">&#949;</span><span class="w"> </span><span class="bp">&gt;</span><span class="w"> </span><span class="mi">0</span><span class="o">,</span><span class="w"> </span><span class="n">ball</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="n">&#949;</span><span class="w"> </span><span class="bp">&#8838;</span><span class="w"> </span><span class="n">interior</span><span class="w"> </span><span class="o">(</span><span class="n">e</span><span class="w"> </span><span class="n">m</span><span class="o">)</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="gr">sorry</span>
<span class="w">  </span><span class="n">obtain</span><span class="w"> </span><span class="o">&#10216;</span><span class="n">k</span><span class="o">,</span><span class="w"> </span><span class="n">hk</span><span class="o">&#10217;</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="bp">&#8707;</span><span class="w"> </span><span class="n">k</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#120156;</span><span class="o">,</span><span class="w"> </span><span class="mi">1</span><span class="w"> </span><span class="bp">&lt;</span><span class="w"> </span><span class="bp">&#8214;</span><span class="n">k</span><span class="bp">&#8214;</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="gr">sorry</span>
<span class="w">  </span><span class="c1">-- show all elements in the ball have norm bounded by `m` after applying any `g i`</span>
<span class="w">  </span><span class="k">have</span><span class="w"> </span><span class="n">real_norm_le</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="bp">&#8704;</span><span class="w"> </span><span class="n">z</span><span class="w"> </span><span class="bp">&#8712;</span><span class="w"> </span><span class="n">ball</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="n">&#949;</span><span class="o">,</span><span class="w"> </span><span class="bp">&#8704;</span><span class="w"> </span><span class="o">(</span><span class="n">i</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#953;</span><span class="o">),</span><span class="w"> </span><span class="bp">&#8214;</span><span class="n">g</span><span class="w"> </span><span class="n">i</span><span class="w"> </span><span class="n">z</span><span class="bp">&#8214;</span><span class="w"> </span><span class="bp">&#8804;</span><span class="w"> </span><span class="n">m</span>
<span class="w">  </span><span class="gr">sorry</span>
<span class="w">  </span><span class="k">have</span><span class="w"> </span><span class="n">&#949;k_pos</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="mi">0</span><span class="w"> </span><span class="bp">&lt;</span><span class="w"> </span><span class="n">&#949;</span><span class="w"> </span><span class="bp">/</span><span class="w"> </span><span class="bp">&#8214;</span><span class="n">k</span><span class="bp">&#8214;</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="gr">sorry</span>
<span class="w">  </span><span class="n">refine</span><span class="w"> </span><span class="o">&#10216;(</span><span class="n">m</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="n">m</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#8469;</span><span class="o">)</span><span class="w"> </span><span class="bp">/</span><span class="w"> </span><span class="o">(</span><span class="n">&#949;</span><span class="w"> </span><span class="bp">/</span><span class="w"> </span><span class="bp">&#8214;</span><span class="n">k</span><span class="bp">&#8214;</span><span class="o">),</span><span class="w"> </span><span class="k">fun</span><span class="w"> </span><span class="n">i</span><span class="w"> </span><span class="bp">&#8614;</span><span class="w"> </span><span class="n">ContinuousLinearMap.opNorm_le_of_shell</span><span class="w"> </span><span class="n">&#949;_pos</span><span class="w"> </span><span class="bp">?</span><span class="n">_</span><span class="w"> </span><span class="n">hk</span><span class="w"> </span><span class="bp">?</span><span class="n">_</span><span class="o">&#10217;</span>
<span class="w">  </span><span class="gr">sorry</span>
<span class="w">  </span><span class="gr">sorry</span>
</pre></div>
</div>
</section>
<section id="asymptotic-comparisons">
<h3><span class="section-number">12.2.3. </span>Asymptotic comparisons<a class="headerlink" href="#asymptotic-comparisons" title="Link to this heading">&#61633;</a></h3>
<p>Defining differentiability also requires asymptotic comparisons.
Mathlib has an extensive library covering the big O and little o relations,
whose definitions are shown below.
Opening the <code class="docutils literal notranslate"><span class="pre">asymptotics</span></code> locale allows us to use the corresponding
notation.
Here we will only use little o to define differentiability.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kn">open</span><span class="w"> </span><span class="n">Asymptotics</span>

<span class="kd">example</span><span class="w"> </span><span class="o">{</span><span class="n">&#945;</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="kt">Type</span><span class="bp">*</span><span class="o">}</span><span class="w"> </span><span class="o">{</span><span class="n">E</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="kt">Type</span><span class="bp">*</span><span class="o">}</span><span class="w"> </span><span class="o">[</span><span class="n">NormedGroup</span><span class="w"> </span><span class="n">E</span><span class="o">]</span><span class="w"> </span><span class="o">{</span><span class="n">F</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="kt">Type</span><span class="bp">*</span><span class="o">}</span><span class="w"> </span><span class="o">[</span><span class="n">NormedGroup</span><span class="w"> </span><span class="n">F</span><span class="o">]</span><span class="w"> </span><span class="o">(</span><span class="n">c</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#8477;</span><span class="o">)</span>
<span class="w">    </span><span class="o">(</span><span class="n">l</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Filter</span><span class="w"> </span><span class="n">&#945;</span><span class="o">)</span><span class="w"> </span><span class="o">(</span><span class="n">f</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#945;</span><span class="w"> </span><span class="bp">&#8594;</span><span class="w"> </span><span class="n">E</span><span class="o">)</span><span class="w"> </span><span class="o">(</span><span class="n">g</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#945;</span><span class="w"> </span><span class="bp">&#8594;</span><span class="w"> </span><span class="n">F</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">IsBigOWith</span><span class="w"> </span><span class="n">c</span><span class="w"> </span><span class="n">l</span><span class="w"> </span><span class="n">f</span><span class="w"> </span><span class="n">g</span><span class="w"> </span><span class="bp">&#8596;</span><span class="w"> </span><span class="bp">&#8704;&#7584;</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="k">in</span><span class="w"> </span><span class="n">l</span><span class="o">,</span><span class="w"> </span><span class="bp">&#8214;</span><span class="n">f</span><span class="w"> </span><span class="n">x</span><span class="bp">&#8214;</span><span class="w"> </span><span class="bp">&#8804;</span><span class="w"> </span><span class="n">c</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="bp">&#8214;</span><span class="n">g</span><span class="w"> </span><span class="n">x</span><span class="bp">&#8214;</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="n">isBigOWith_iff</span>

<span class="kd">example</span><span class="w"> </span><span class="o">{</span><span class="n">&#945;</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="kt">Type</span><span class="bp">*</span><span class="o">}</span><span class="w"> </span><span class="o">{</span><span class="n">E</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="kt">Type</span><span class="bp">*</span><span class="o">}</span><span class="w"> </span><span class="o">[</span><span class="n">NormedGroup</span><span class="w"> </span><span class="n">E</span><span class="o">]</span><span class="w"> </span><span class="o">{</span><span class="n">F</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="kt">Type</span><span class="bp">*</span><span class="o">}</span><span class="w"> </span><span class="o">[</span><span class="n">NormedGroup</span><span class="w"> </span><span class="n">F</span><span class="o">]</span>
<span class="w">    </span><span class="o">(</span><span class="n">l</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Filter</span><span class="w"> </span><span class="n">&#945;</span><span class="o">)</span><span class="w"> </span><span class="o">(</span><span class="n">f</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#945;</span><span class="w"> </span><span class="bp">&#8594;</span><span class="w"> </span><span class="n">E</span><span class="o">)</span><span class="w"> </span><span class="o">(</span><span class="n">g</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#945;</span><span class="w"> </span><span class="bp">&#8594;</span><span class="w"> </span><span class="n">F</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">f</span><span class="w"> </span><span class="bp">=</span><span class="n">O</span><span class="o">[</span><span class="n">l</span><span class="o">]</span><span class="w"> </span><span class="n">g</span><span class="w"> </span><span class="bp">&#8596;</span><span class="w"> </span><span class="bp">&#8707;</span><span class="w"> </span><span class="n">C</span><span class="o">,</span><span class="w"> </span><span class="n">IsBigOWith</span><span class="w"> </span><span class="n">C</span><span class="w"> </span><span class="n">l</span><span class="w"> </span><span class="n">f</span><span class="w"> </span><span class="n">g</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="n">isBigO_iff_isBigOWith</span>

<span class="kd">example</span><span class="w"> </span><span class="o">{</span><span class="n">&#945;</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="kt">Type</span><span class="bp">*</span><span class="o">}</span><span class="w"> </span><span class="o">{</span><span class="n">E</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="kt">Type</span><span class="bp">*</span><span class="o">}</span><span class="w"> </span><span class="o">[</span><span class="n">NormedGroup</span><span class="w"> </span><span class="n">E</span><span class="o">]</span><span class="w"> </span><span class="o">{</span><span class="n">F</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="kt">Type</span><span class="bp">*</span><span class="o">}</span><span class="w"> </span><span class="o">[</span><span class="n">NormedGroup</span><span class="w"> </span><span class="n">F</span><span class="o">]</span>
<span class="w">    </span><span class="o">(</span><span class="n">l</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Filter</span><span class="w"> </span><span class="n">&#945;</span><span class="o">)</span><span class="w"> </span><span class="o">(</span><span class="n">f</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#945;</span><span class="w"> </span><span class="bp">&#8594;</span><span class="w"> </span><span class="n">E</span><span class="o">)</span><span class="w"> </span><span class="o">(</span><span class="n">g</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#945;</span><span class="w"> </span><span class="bp">&#8594;</span><span class="w"> </span><span class="n">F</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">f</span><span class="w"> </span><span class="bp">=</span><span class="n">o</span><span class="o">[</span><span class="n">l</span><span class="o">]</span><span class="w"> </span><span class="n">g</span><span class="w"> </span><span class="bp">&#8596;</span><span class="w"> </span><span class="bp">&#8704;</span><span class="w"> </span><span class="n">C</span><span class="w"> </span><span class="bp">&gt;</span><span class="w"> </span><span class="mi">0</span><span class="o">,</span><span class="w"> </span><span class="n">IsBigOWith</span><span class="w"> </span><span class="n">C</span><span class="w"> </span><span class="n">l</span><span class="w"> </span><span class="n">f</span><span class="w"> </span><span class="n">g</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="n">isLittleO_iff_forall_isBigOWith</span>

<span class="kd">example</span><span class="w"> </span><span class="o">{</span><span class="n">&#945;</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="kt">Type</span><span class="bp">*</span><span class="o">}</span><span class="w"> </span><span class="o">{</span><span class="n">E</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="kt">Type</span><span class="bp">*</span><span class="o">}</span><span class="w"> </span><span class="o">[</span><span class="n">NormedAddCommGroup</span><span class="w"> </span><span class="n">E</span><span class="o">]</span><span class="w"> </span><span class="o">(</span><span class="n">l</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Filter</span><span class="w"> </span><span class="n">&#945;</span><span class="o">)</span><span class="w"> </span><span class="o">(</span><span class="n">f</span><span class="w"> </span><span class="n">g</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#945;</span><span class="w"> </span><span class="bp">&#8594;</span><span class="w"> </span><span class="n">E</span><span class="o">)</span><span class="w"> </span><span class="o">:</span>
<span class="w">    </span><span class="n">f</span><span class="w"> </span><span class="bp">~</span><span class="o">[</span><span class="n">l</span><span class="o">]</span><span class="w"> </span><span class="n">g</span><span class="w"> </span><span class="bp">&#8596;</span><span class="w"> </span><span class="o">(</span><span class="n">f</span><span class="w"> </span><span class="bp">-</span><span class="w"> </span><span class="n">g</span><span class="o">)</span><span class="w"> </span><span class="bp">=</span><span class="n">o</span><span class="o">[</span><span class="n">l</span><span class="o">]</span><span class="w"> </span><span class="n">g</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="n">Iff.rfl</span>
</pre></div>
</div>
</section>
<section id="differentiability">
<h3><span class="section-number">12.2.4. </span>Differentiability<a class="headerlink" href="#differentiability" title="Link to this heading">&#61633;</a></h3>
<p>We are now ready to discuss differentiable functions between normed spaces.
In analogy the elementary one-dimensional,
Mathlib defines a predicate <code class="docutils literal notranslate"><span class="pre">HasFDerivAt</span></code> and a function <code class="docutils literal notranslate"><span class="pre">fderiv</span></code>.
Here the letter
&#8220;f&#8221; stands for <em>Fr&#233;chet</em>.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kn">open</span><span class="w"> </span><span class="n">Topology</span>

<span class="kd">variable</span><span class="w"> </span><span class="o">{</span><span class="n">&#120156;</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="kt">Type</span><span class="bp">*</span><span class="o">}</span><span class="w"> </span><span class="o">[</span><span class="n">NontriviallyNormedField</span><span class="w"> </span><span class="n">&#120156;</span><span class="o">]</span><span class="w"> </span><span class="o">{</span><span class="n">E</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="kt">Type</span><span class="bp">*</span><span class="o">}</span><span class="w"> </span><span class="o">[</span><span class="n">NormedAddCommGroup</span><span class="w"> </span><span class="n">E</span><span class="o">]</span>
<span class="w">  </span><span class="o">[</span><span class="n">NormedSpace</span><span class="w"> </span><span class="n">&#120156;</span><span class="w"> </span><span class="n">E</span><span class="o">]</span><span class="w"> </span><span class="o">{</span><span class="n">F</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="kt">Type</span><span class="bp">*</span><span class="o">}</span><span class="w"> </span><span class="o">[</span><span class="n">NormedAddCommGroup</span><span class="w"> </span><span class="n">F</span><span class="o">]</span><span class="w"> </span><span class="o">[</span><span class="n">NormedSpace</span><span class="w"> </span><span class="n">&#120156;</span><span class="w"> </span><span class="n">F</span><span class="o">]</span>

<span class="kd">example</span><span class="w"> </span><span class="o">(</span><span class="n">f</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">E</span><span class="w"> </span><span class="bp">&#8594;</span><span class="w"> </span><span class="n">F</span><span class="o">)</span><span class="w"> </span><span class="o">(</span><span class="n">f&#39;</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">E</span><span class="w"> </span><span class="bp">&#8594;</span><span class="n">L</span><span class="o">[</span><span class="n">&#120156;</span><span class="o">]</span><span class="w"> </span><span class="n">F</span><span class="o">)</span><span class="w"> </span><span class="o">(</span><span class="n">x&#8320;</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">E</span><span class="o">)</span><span class="w"> </span><span class="o">:</span>
<span class="w">    </span><span class="n">HasFDerivAt</span><span class="w"> </span><span class="n">f</span><span class="w"> </span><span class="n">f&#39;</span><span class="w"> </span><span class="n">x&#8320;</span><span class="w"> </span><span class="bp">&#8596;</span><span class="w"> </span><span class="o">(</span><span class="k">fun</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="bp">&#8614;</span><span class="w"> </span><span class="n">f</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="bp">-</span><span class="w"> </span><span class="n">f</span><span class="w"> </span><span class="n">x&#8320;</span><span class="w"> </span><span class="bp">-</span><span class="w"> </span><span class="n">f&#39;</span><span class="w"> </span><span class="o">(</span><span class="n">x</span><span class="w"> </span><span class="bp">-</span><span class="w"> </span><span class="n">x&#8320;</span><span class="o">))</span><span class="w"> </span><span class="bp">=</span><span class="n">o</span><span class="o">[</span><span class="n">&#120029;</span><span class="w"> </span><span class="n">x&#8320;</span><span class="o">]</span><span class="w"> </span><span class="k">fun</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="bp">&#8614;</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="bp">-</span><span class="w"> </span><span class="n">x&#8320;</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="n">hasFDerivAtFilter_iff_isLittleO</span><span class="w"> </span><span class="bp">..</span>

<span class="kd">example</span><span class="w"> </span><span class="o">(</span><span class="n">f</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">E</span><span class="w"> </span><span class="bp">&#8594;</span><span class="w"> </span><span class="n">F</span><span class="o">)</span><span class="w"> </span><span class="o">(</span><span class="n">f&#39;</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">E</span><span class="w"> </span><span class="bp">&#8594;</span><span class="n">L</span><span class="o">[</span><span class="n">&#120156;</span><span class="o">]</span><span class="w"> </span><span class="n">F</span><span class="o">)</span><span class="w"> </span><span class="o">(</span><span class="n">x&#8320;</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">E</span><span class="o">)</span><span class="w"> </span><span class="o">(</span><span class="n">hff&#39;</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">HasFDerivAt</span><span class="w"> </span><span class="n">f</span><span class="w"> </span><span class="n">f&#39;</span><span class="w"> </span><span class="n">x&#8320;</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">fderiv</span><span class="w"> </span><span class="n">&#120156;</span><span class="w"> </span><span class="n">f</span><span class="w"> </span><span class="n">x&#8320;</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">f&#39;</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="n">hff&#39;.fderiv</span>
</pre></div>
</div>
<p>We also have iterated derivatives that take values in the type of multilinear maps
<code class="docutils literal notranslate"><span class="pre">E</span> <span class="pre">[&#215;n]&#8594;L[&#120156;]</span> <span class="pre">F</span></code>,
and we have continuously differential functions.
The type <code class="docutils literal notranslate"><span class="pre">&#8469;&#8734;</span></code> is <code class="docutils literal notranslate"><span class="pre">&#8469;</span></code> with an additional element <code class="docutils literal notranslate"><span class="pre">&#8734;</span></code> that
is bigger than every natural number.
So <span class="math notranslate nohighlight">\(\mathcal{C}^\infty\)</span> functions are functions <code class="docutils literal notranslate"><span class="pre">f</span></code> that satisfy
<code class="docutils literal notranslate"><span class="pre">ContDiff</span> <span class="pre">&#120156;</span> <span class="pre">&#8868;</span> <span class="pre">f</span></code>.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span><span class="w"> </span><span class="o">(</span><span class="n">n</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#8469;</span><span class="o">)</span><span class="w"> </span><span class="o">(</span><span class="n">f</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">E</span><span class="w"> </span><span class="bp">&#8594;</span><span class="w"> </span><span class="n">F</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">E</span><span class="w"> </span><span class="bp">&#8594;</span><span class="w"> </span><span class="n">E</span><span class="o">[</span><span class="bp">&#215;</span><span class="n">n</span><span class="o">]</span><span class="bp">&#8594;</span><span class="n">L</span><span class="o">[</span><span class="n">&#120156;</span><span class="o">]</span><span class="w"> </span><span class="n">F</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="n">iteratedFDeriv</span><span class="w"> </span><span class="n">&#120156;</span><span class="w"> </span><span class="n">n</span><span class="w"> </span><span class="n">f</span>

<span class="kd">example</span><span class="w"> </span><span class="o">(</span><span class="n">n</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#8469;</span><span class="bp">&#8734;</span><span class="o">)</span><span class="w"> </span><span class="o">{</span><span class="n">f</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">E</span><span class="w"> </span><span class="bp">&#8594;</span><span class="w"> </span><span class="n">F</span><span class="o">}</span><span class="w"> </span><span class="o">:</span>
<span class="w">    </span><span class="n">ContDiff</span><span class="w"> </span><span class="n">&#120156;</span><span class="w"> </span><span class="n">n</span><span class="w"> </span><span class="n">f</span><span class="w"> </span><span class="bp">&#8596;</span>
<span class="w">      </span><span class="o">(</span><span class="bp">&#8704;</span><span class="w"> </span><span class="n">m</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#8469;</span><span class="o">,</span><span class="w"> </span><span class="o">(</span><span class="n">m</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">WithTop</span><span class="w"> </span><span class="n">&#8469;</span><span class="o">)</span><span class="w"> </span><span class="bp">&#8804;</span><span class="w"> </span><span class="n">n</span><span class="w"> </span><span class="bp">&#8594;</span><span class="w"> </span><span class="n">Continuous</span><span class="w"> </span><span class="k">fun</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="bp">&#8614;</span><span class="w"> </span><span class="n">iteratedFDeriv</span><span class="w"> </span><span class="n">&#120156;</span><span class="w"> </span><span class="n">m</span><span class="w"> </span><span class="n">f</span><span class="w"> </span><span class="n">x</span><span class="o">)</span><span class="w"> </span><span class="bp">&#8743;</span>
<span class="w">        </span><span class="bp">&#8704;</span><span class="w"> </span><span class="n">m</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#8469;</span><span class="o">,</span><span class="w"> </span><span class="o">(</span><span class="n">m</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">WithTop</span><span class="w"> </span><span class="n">&#8469;</span><span class="o">)</span><span class="w"> </span><span class="bp">&lt;</span><span class="w"> </span><span class="n">n</span><span class="w"> </span><span class="bp">&#8594;</span><span class="w"> </span><span class="n">Differentiable</span><span class="w"> </span><span class="n">&#120156;</span><span class="w"> </span><span class="k">fun</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="bp">&#8614;</span><span class="w"> </span><span class="n">iteratedFDeriv</span><span class="w"> </span><span class="n">&#120156;</span><span class="w"> </span><span class="n">m</span><span class="w"> </span><span class="n">f</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="n">contDiff_iff_continuous_differentiable</span>
</pre></div>
</div>
<p>The differentiability parameter in <code class="docutils literal notranslate"><span class="pre">ContDiff</span></code> can also take value <code class="docutils literal notranslate"><span class="pre">&#969;</span> <span class="pre">:</span> <span class="pre">WithTop</span> <span class="pre">&#8469;&#8734;</span></code>
to denote analytic functions.</p>
<p>There is a stricter notion of differentiability called
<code class="docutils literal notranslate"><span class="pre">HasStrictFDerivAt</span></code>, which is used in the statement
of the inverse function theorem and the statement of the implicit function
theorem, both of which are in Mathlib.
Over <code class="docutils literal notranslate"><span class="pre">&#8477;</span></code> or <code class="docutils literal notranslate"><span class="pre">&#8450;</span></code>, continuously differentiable
functions are strictly differentiable.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span><span class="w"> </span><span class="o">{</span><span class="n">&#120130;</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="kt">Type</span><span class="bp">*</span><span class="o">}</span><span class="w"> </span><span class="o">[</span><span class="n">RCLike</span><span class="w"> </span><span class="n">&#120130;</span><span class="o">]</span><span class="w"> </span><span class="o">{</span><span class="n">E</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="kt">Type</span><span class="bp">*</span><span class="o">}</span><span class="w"> </span><span class="o">[</span><span class="n">NormedAddCommGroup</span><span class="w"> </span><span class="n">E</span><span class="o">]</span><span class="w"> </span><span class="o">[</span><span class="n">NormedSpace</span><span class="w"> </span><span class="n">&#120130;</span><span class="w"> </span><span class="n">E</span><span class="o">]</span><span class="w"> </span><span class="o">{</span><span class="n">F</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="kt">Type</span><span class="bp">*</span><span class="o">}</span>
<span class="w">    </span><span class="o">[</span><span class="n">NormedAddCommGroup</span><span class="w"> </span><span class="n">F</span><span class="o">]</span><span class="w"> </span><span class="o">[</span><span class="n">NormedSpace</span><span class="w"> </span><span class="n">&#120130;</span><span class="w"> </span><span class="n">F</span><span class="o">]</span><span class="w"> </span><span class="o">{</span><span class="n">f</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">E</span><span class="w"> </span><span class="bp">&#8594;</span><span class="w"> </span><span class="n">F</span><span class="o">}</span><span class="w"> </span><span class="o">{</span><span class="n">x</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">E</span><span class="o">}</span><span class="w"> </span><span class="o">{</span><span class="n">n</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">WithTop</span><span class="w"> </span><span class="n">&#8469;</span><span class="bp">&#8734;</span><span class="o">}</span>
<span class="w">    </span><span class="o">(</span><span class="n">hf</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">ContDiffAt</span><span class="w"> </span><span class="n">&#120130;</span><span class="w"> </span><span class="n">n</span><span class="w"> </span><span class="n">f</span><span class="w"> </span><span class="n">x</span><span class="o">)</span><span class="w"> </span><span class="o">(</span><span class="n">hn</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="mi">1</span><span class="w"> </span><span class="bp">&#8804;</span><span class="w"> </span><span class="n">n</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">HasStrictFDerivAt</span><span class="w"> </span><span class="n">f</span><span class="w"> </span><span class="o">(</span><span class="n">fderiv</span><span class="w"> </span><span class="n">&#120130;</span><span class="w"> </span><span class="n">f</span><span class="w"> </span><span class="n">x</span><span class="o">)</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="n">hf.hasStrictFDerivAt</span><span class="w"> </span><span class="n">hn</span>
</pre></div>
</div>
<p>The local inverse theorem is stated using an operation that produces an
inverse function from a
function and the assumptions that the function is strictly differentiable at a
point <code class="docutils literal notranslate"><span class="pre">a</span></code> and that its derivative is an isomorphism.</p>
<p>The first example below gets this local inverse.
The next one states that it is indeed a local inverse
from the left and from the right, and that it is strictly differentiable.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kn">section</span><span class="w"> </span><span class="n">LocalInverse</span>
<span class="kd">variable</span><span class="w"> </span><span class="o">[</span><span class="n">CompleteSpace</span><span class="w"> </span><span class="n">E</span><span class="o">]</span><span class="w"> </span><span class="o">{</span><span class="n">f</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">E</span><span class="w"> </span><span class="bp">&#8594;</span><span class="w"> </span><span class="n">F</span><span class="o">}</span><span class="w"> </span><span class="o">{</span><span class="n">f&#39;</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">E</span><span class="w"> </span><span class="bp">&#8771;</span><span class="n">L</span><span class="o">[</span><span class="n">&#120156;</span><span class="o">]</span><span class="w"> </span><span class="n">F</span><span class="o">}</span><span class="w"> </span><span class="o">{</span><span class="n">a</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">E</span><span class="o">}</span>

<span class="kd">example</span><span class="w"> </span><span class="o">(</span><span class="n">hf</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">HasStrictFDerivAt</span><span class="w"> </span><span class="n">f</span><span class="w"> </span><span class="o">(</span><span class="n">f&#39;</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">E</span><span class="w"> </span><span class="bp">&#8594;</span><span class="n">L</span><span class="o">[</span><span class="n">&#120156;</span><span class="o">]</span><span class="w"> </span><span class="n">F</span><span class="o">)</span><span class="w"> </span><span class="n">a</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">F</span><span class="w"> </span><span class="bp">&#8594;</span><span class="w"> </span><span class="n">E</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="n">HasStrictFDerivAt.localInverse</span><span class="w"> </span><span class="n">f</span><span class="w"> </span><span class="n">f&#39;</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="n">hf</span>

<span class="kd">example</span><span class="w"> </span><span class="o">(</span><span class="n">hf</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">HasStrictFDerivAt</span><span class="w"> </span><span class="n">f</span><span class="w"> </span><span class="o">(</span><span class="n">f&#39;</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">E</span><span class="w"> </span><span class="bp">&#8594;</span><span class="n">L</span><span class="o">[</span><span class="n">&#120156;</span><span class="o">]</span><span class="w"> </span><span class="n">F</span><span class="o">)</span><span class="w"> </span><span class="n">a</span><span class="o">)</span><span class="w"> </span><span class="o">:</span>
<span class="w">    </span><span class="bp">&#8704;&#7584;</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="k">in</span><span class="w"> </span><span class="n">&#120029;</span><span class="w"> </span><span class="n">a</span><span class="o">,</span><span class="w"> </span><span class="n">hf.localInverse</span><span class="w"> </span><span class="n">f</span><span class="w"> </span><span class="n">f&#39;</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="o">(</span><span class="n">f</span><span class="w"> </span><span class="n">x</span><span class="o">)</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="n">hf.eventually_left_inverse</span>

<span class="kd">example</span><span class="w"> </span><span class="o">(</span><span class="n">hf</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">HasStrictFDerivAt</span><span class="w"> </span><span class="n">f</span><span class="w"> </span><span class="o">(</span><span class="n">f&#39;</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">E</span><span class="w"> </span><span class="bp">&#8594;</span><span class="n">L</span><span class="o">[</span><span class="n">&#120156;</span><span class="o">]</span><span class="w"> </span><span class="n">F</span><span class="o">)</span><span class="w"> </span><span class="n">a</span><span class="o">)</span><span class="w"> </span><span class="o">:</span>
<span class="w">    </span><span class="bp">&#8704;&#7584;</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="k">in</span><span class="w"> </span><span class="n">&#120029;</span><span class="w"> </span><span class="o">(</span><span class="n">f</span><span class="w"> </span><span class="n">a</span><span class="o">),</span><span class="w"> </span><span class="n">f</span><span class="w"> </span><span class="o">(</span><span class="n">hf.localInverse</span><span class="w"> </span><span class="n">f</span><span class="w"> </span><span class="n">f&#39;</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="n">x</span><span class="o">)</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="n">hf.eventually_right_inverse</span>

<span class="kd">example</span><span class="w"> </span><span class="o">{</span><span class="n">f</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">E</span><span class="w"> </span><span class="bp">&#8594;</span><span class="w"> </span><span class="n">F</span><span class="o">}</span><span class="w"> </span><span class="o">{</span><span class="n">f&#39;</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">E</span><span class="w"> </span><span class="bp">&#8771;</span><span class="n">L</span><span class="o">[</span><span class="n">&#120156;</span><span class="o">]</span><span class="w"> </span><span class="n">F</span><span class="o">}</span><span class="w"> </span><span class="o">{</span><span class="n">a</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">E</span><span class="o">}</span>
<span class="w">  </span><span class="o">(</span><span class="n">hf</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">HasStrictFDerivAt</span><span class="w"> </span><span class="n">f</span><span class="w"> </span><span class="o">(</span><span class="n">f&#39;</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">E</span><span class="w"> </span><span class="bp">&#8594;</span><span class="n">L</span><span class="o">[</span><span class="n">&#120156;</span><span class="o">]</span><span class="w"> </span><span class="n">F</span><span class="o">)</span><span class="w"> </span><span class="n">a</span><span class="o">)</span><span class="w"> </span><span class="o">:</span>
<span class="w">    </span><span class="n">HasStrictFDerivAt</span><span class="w"> </span><span class="o">(</span><span class="n">HasStrictFDerivAt.localInverse</span><span class="w"> </span><span class="n">f</span><span class="w"> </span><span class="n">f&#39;</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="n">hf</span><span class="o">)</span><span class="w"> </span><span class="o">(</span><span class="n">f&#39;.symm</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">F</span><span class="w"> </span><span class="bp">&#8594;</span><span class="n">L</span><span class="o">[</span><span class="n">&#120156;</span><span class="o">]</span><span class="w"> </span><span class="n">E</span><span class="o">)</span><span class="w"> </span><span class="o">(</span><span class="n">f</span><span class="w"> </span><span class="n">a</span><span class="o">)</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="n">HasStrictFDerivAt.to_localInverse</span><span class="w"> </span><span class="n">hf</span>

<span class="kd">end</span><span class="w"> </span><span class="n">LocalInverse</span>
</pre></div>
</div>
<p>This has been only a quick tour of the differential calculus in Mathlib.
The library contains many variations that we have not discussed.
For example, you may want to use one-sided derivatives in the
one-dimensional setting. The means to do so are found in Mathlib in a more
general context;
see <code class="docutils literal notranslate"><span class="pre">HasFDerivWithinAt</span></code> or the even more general <code class="docutils literal notranslate"><span class="pre">HasFDerivAtFilter</span></code>.</p>
</section>
</section>
</section>


           </div>
          </div>
          <footer><div class="rst-footer-buttons" role="navigation" aria-label="Footer">
        <a href="C11_Topology.html" class="btn btn-neutral float-left" title="11. Topology" accesskey="p" rel="prev"><span class="fa fa-arrow-circle-left" aria-hidden="true"></span> Previous</a>
        <a href="C13_Integration_and_Measure_Theory.html" class="btn btn-neutral float-right" title="13. Integration and Measure Theory" accesskey="n" rel="next">Next <span class="fa fa-arrow-circle-right" aria-hidden="true"></span></a>
    </div>

  <hr/>

  <div role="contentinfo">
    <p>&#169; Copyright 2020-2025, Jeremy Avigad, Patrick Massot. Text licensed under CC BY 4.0.</p>
  </div>

  Built with <a href="https://www.sphinx-doc.org/">Sphinx</a> using a
    <a href="https://github.com/readthedocs/sphinx_rtd_theme">theme</a>
    provided by <a href="https://readthedocs.org">Read the Docs</a>.
   

</footer>
        </div>
      </div>
    </section>
  </div>
  <script>
      jQuery(function () {
          SphinxRtdTheme.Navigation.enable(true);
      });
  </script> 

</body>
</html>